Nuprl Lemma : decidable__same-thread
11,40
postcript
pdf
es
:ES,
p
:(E
(E + Top)). causal-predecessor(
es
;
p
)
(
e
,
e'
:E. Dec(same-thread(
es
;
p
;
e
;
e'
)))
latex
Definitions
t
T
,
same-thread(
es
;
p
;
e
;
e'
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
Lemmas
event
system
wf
,
top
wf
,
causal-predecessor
wf
,
es-E
wf
,
final-iterate
wf
,
decidable
es-E-equal
,
causal-pred-wellfounded
origin
es:ES, p:(E
(E + Top)). causal-predecessor(es;p) 
(e, e':E. Dec(same-thread(es;p;e;e'))) es:ES, p:(E(E + Top)). causal-predecessor(es;p) (e, e':E. Dec(same-thread(es;p;e;e'))) 
T Qx:A. B(x)